/* Benchmarks for the PionterC */

// list definition

struct list
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @                  (({l}) && list(l->next))
  @ in  list(l)
  @ end
  @*/

struct list* test_if(struct list* l)
{
  int s;
  
  if (l==null)
    s = 0;
  else s = l->data;
  return l;
}
/*@ list(result) */

/*@*/
int main ()
{
  test_if (null);
  return 0;
}
/*@*/
